
#include "NodeParallel.h"
#include "Node.h"
#include <vector>
#include <iostream>
using namespace std;

__device__ inline bool isSolved(NodeParallel node)
{
	return *(node.bitmap) & (1 << 0);
}

__device__ inline bool isSolvable(NodeParallel node)
{
	return *(node.bitmap) & (1 << 1);
}

__device__ inline bool varAffected(NodeParallel node, int i)
{
	return *(node.b1 + i / 8) & (1 << i % 8);
}

__device__ inline bool varValues(NodeParallel node, int i)
{
	return *(node.b2 + i / 8) & (1 << i % 8);
}

__device__ inline bool solvedClauses(NodeParallel node, int i)
{
	return *(node.b3 + i / 8) & (1 << i % 8);
}

__device__ inline bool clauseLiterals(NodeParallel node, int k, int i)
{
	return *(node.b4 + (k + i * node.m) / 8) & (1 << (k + i * node.m) % 8);
}

__device__ inline void set_solved(NodeParallel node, bool val)
{
	if (isSolved(node) != val)
	{
		*(node.bitmap) ^= (1 << 0);
	}
}

__device__ inline void set_solvable(NodeParallel node, bool val)
{
	if (isSolvable(node) != val)
	{
		*(node.bitmap) ^= (1 << 1);
	}
}

__device__ inline void set_varAffected(NodeParallel node, int i, bool val)
{
	if (varAffected(node, i) != val)
	{
		*(node.b1 + i / 8) ^= (1 << i % 8);
	}
}

__device__ inline void set_varValues(NodeParallel node, int i, bool val)
{
	if (varValues(node, i) != val)
	{
		*(node.b2 + i / 8) ^= (1 << i % 8);
	}
}

__device__ inline void set_solvedClauses(NodeParallel node, int i, bool val)
{
	if (solvedClauses(node, i) != val)
	{
		*(node.b3 + i / 8) ^= (1 << i % 8);
	}
}

__device__ inline void set_clauseLiterals(NodeParallel node, int k, int i, bool val)
{
	if (clauseLiterals(node, k, i) != val)
	{
		*(node.b4 + (k + i * node.m) / 8) ^= (1 << (k + i * node.m) % 8);
	}
}

__device__ inline int negation (NodeParallel node, int i)
{
	return 2 * node.n - 1 - i;
}

__device__ NodeParallel buildNode(char *output, char *b, int a_n, int a_m)
{
	NodeParallel node;
	node.n = a_n;
	node.m = a_m;
	node.o = 2*a_n*a_m;
	
	size_t memory_n = (a_n % 8 == 0 ? a_n / 8 : a_n / 8 + 1);
	size_t memory_m = (a_m % 8 == 0 ? a_m / 8 : a_m / 8 + 1);
	size_t memory_nm = (2*a_n*a_m % 8 == 0 ? 2*a_n*a_m / 8 : 2*a_n*a_m / 8 + 1);
	
	node.bitmap = output;
	
	node.b1 = node.bitmap + 1;
	node.b2 = node.b1 + memory_n;
	node.b3 = node.b2 + memory_n;
	node.b4 = node.b3 + memory_m;
	
	memcpy(node.bitmap, b, 1 + 2 * memory_n + memory_m + memory_nm);
	
	return(node);
}


__global__ void exploreOneParallel (char* output, char* b, int *vars, int n,
									int m, int N, size_t allocated_size,
									size_t queues_size, int * toAffect_buffer,
									bool * temp_buffer,
									int * toPropagate_buffer,
									int * recentlySolved_buffer,
									char * possiblyDisappeared_buffer)
{
	int i = blockIdx.x * blockDim.x + threadIdx.x;
	
	if(i >= (1 << N))
	{
		return;
	}
	
	NodeParallel result = buildNode(output+i*allocated_size, b,n,m);
	
	//First, we build a list of variables to affect
	QueueInt toAffect = newQueueInt(toAffect_buffer + queues_size * i,
									queues_size);
	for(int j = 0; j<N; j++)
	{
		add(toAffect, vars[j]);
	}
	
	//Then, we use index of the new node to determine which variables will be set to true or false
	QueueBool temp = newQueueBool(temp_buffer + queues_size * i, queues_size);
	
	for(int j=0; j < N; j++)
	{
		if((i & (1<<j)) != 0)
		{
			add(temp, true);
		}
		else
		{
			add(temp, false);
		}
	}
	
	//This variable will let us know when a clause
	//will have been statisfied, so that we can check
	//if the problem is solved
	bool solvedOneClause = false;
	
	//List of conditions that may help propagate the affectation
	QueueInt toPropagate = newQueueInt(toPropagate_buffer + m * i, m);
	//List of clauses that were just solved
	QueueInt recentlySolved = newQueueInt(recentlySolved_buffer + m * i, m);
	

	int currentVar;
	bool currentValue;
	
	while(!isEmpty(toAffect))
	{
		currentVar = poll(toAffect);
		currentValue = poll(temp);
		
		//We check that there is no conflict in affectations
		if(varAffected(result, currentVar))
		{
			if(varValues(result, currentVar) != currentValue)
			{
				set_solvable(result, false);
				return;
			}
			else
			{
				continue;
			}
		}
		
		//If not, we can affect it
		set_varAffected(result, currentVar,true);
		set_varValues(result, currentVar, currentValue);
		
		//Each time we affect a variable, we check the unsatisfied clauses containing it
		for(int k=0; k < m; k++)
		{
			if(!solvedClauses(result, k))
			{
				//If the affectation did not satisfy the clause, we remove the variable
				//from the remaining literals of the clause. If it did, we mark the clause
				//as satisfied
				if(clauseLiterals(result, k, currentVar))
				{
					if(currentValue)
					{
						set_solvedClauses(result, k, true);
						solvedOneClause = true;
						add(recentlySolved, k);
					}
					else
					{
						add(toPropagate, k);
						set_clauseLiterals(result, k, currentVar, false);
					}
				}
				else if(clauseLiterals(result, k, negation(result, currentVar)))
				{
					if(!currentValue)
					{
						set_solvedClauses(result, k, true);
						solvedOneClause = true;
						add(recentlySolved, k);
					}
					else
					{
						add(toPropagate,k);
						set_clauseLiterals(result, k, negation(result, currentVar), false);
					}
				}
			}
		}
		
		//Now for the propagation
		int k, remainingLiterals, variable;
		bool valVariable;
		
		while(!isEmpty(toPropagate))
		{
			k = poll(toPropagate);
			
			//We count the number of remaining literals in the modified clauses
			remainingLiterals = 0;
			
			for(int l=0; l<2*n; l++)
			{
				if(clauseLiterals(result, k, l))
				{
					remainingLiterals++;
					if(remainingLiterals > 1)
					{
						break;
					}
					
					if(l<result.n)
					{
						variable = l;
						valVariable = true;
					}
					else
					{
						variable = negation(result, l);
						valVariable = false;
					}
				}
			}
			
			//If there are no literals left, the node is not solvable
			//If there is only one left, we can affect it
			if(remainingLiterals == 0)
			{
				set_solvable(result, false);
				return;
			}
			else if (remainingLiterals == 1)
			{
				add(toAffect, variable);
				add(temp, valVariable);
			}
		}
		
		//Now we will affect literals which don't have their negations in the formula anymore
		Bitmap possiblyDisappeared =
			newBitmap(possiblyDisappeared_buffer + ((2 * n) % 8 == 0 ?
													(2 * n) / 8 :
													(2 * n) / 8 + 1) * i,
					  2 * n);
		
		int possiblyDisappearedNumber = 0;
		
		// Get the literals that have possibly disappeared from the clauses that
		// were solved during that iteration of the loop
		
		while(isEmpty(toAffect) && !isEmpty(recentlySolved))
		{
			k = poll(recentlySolved);
			
			for(int l=0; l<2*n; l++)
			{
				if (l < n && !varAffected(result, l) ||
					l >= n && !varAffected(result, negation(result, l)))
				{
					if(clauseLiterals(result, k, l))
					{
						if(!get(possiblyDisappeared, l))
						{
							setBitmap(possiblyDisappeared, l, true);
							possiblyDisappearedNumber++;
						}
					}
				}
			}
		}
		
		// Now get the literals that have really disappeared from those that
		// have possibly disappeared
		if(possiblyDisappearedNumber > 0)
		{
			for(k=0; k < m; k++)
			{
				if(!solvedClauses(result, k))
				{
					for(int l=0; l<2*n; l++)
					{
						if(clauseLiterals(result, k, l))
						{
							if(get(possiblyDisappeared, l))
							{
								setBitmap(possiblyDisappeared, l, false);
								possiblyDisappearedNumber--;
								if(possiblyDisappearedNumber == 0)
								{
									break;
								}
							}
						}
					}
				}
			}
		}
		
		// For all literals that have disappeared, affect its negation
		// (therefore a pure literal) to true
		if(possiblyDisappearedNumber > 0)
		{
			for(k=0; k<2*n; k++)
			{
				if(get(possiblyDisappeared, k))
				{
					if(k<n)
					{
						add(toAffect, k);
						add(temp, false);
					}
					else
					{
						add(toAffect, negation(result, k));
						add(temp, true);
					}
				}
			}
		}
		
	}
	
	//If we have satisfied a new clause, we check if the problem is solved
	if(isSolvable(result) && solvedOneClause)
	{
		set_solved(result, true);
		for(int j=0; j < m; j++)
		{
			if(!solvedClauses(result, j))
			{
				set_solved(result, false);
				break;
			}
		}
	}
}

__host__ void testError(int line)
{
	cudaError_t error;
	if((error = cudaGetLastError()) != cudaSuccess)
	{
		cerr<<"Ooops, an error occured (l."<<line<<"): "<<cudaGetErrorString(error)<<endl;
		exit(EXIT_FAILURE);
	}
}

__host__ vector<Node> Node::exploreParallel(unsigned int N)
{
	vector<Node> result;
	
	/* First simplify the current node, if the formula has been satisfied by
	 simplification, just return the current node.
	 */
	if (isSolved())
	{
		result.push_back(*this);
	}
	
	/* Else, branch on the given number of next unaffected variables. */
	else
	{
		unaffected(N);
		
		if(isSolvable())    //If the problem is not solvable, we don't create new nodes
		{
			//We branch on vars.size() binary variables
			int nbNewNodes = 1 << nbSelected;

			//Memory allocation
			char *device_bitmap;
			int *device_vars;
			char *device_output;
			int * toAffect_buffer;
			bool * temp_buffer;
			int * toPropagate_buffer;
			int * recentlySolved_buffer;
			char * possiblyDisappeared_buffer;
			
			size_t queues_size = 2 * n;
			cudaMalloc(&device_bitmap, allocated_size);							testError(__LINE__);
			cudaMalloc(&device_vars, nbSelected*sizeof(int));					testError(__LINE__);
			cudaMalloc(&device_output, nbNewNodes*allocated_size);				testError(__LINE__);
			cudaMalloc(&toAffect_buffer,
					   nbNewNodes * queues_size * sizeof(int));				testError(__LINE__);
			cudaMalloc(&temp_buffer, nbNewNodes * queues_size * sizeof(bool));				testError(__LINE__);
			cudaMalloc(&toPropagate_buffer, nbNewNodes * m * sizeof(int));				testError(__LINE__);
			cudaMalloc(&recentlySolved_buffer, nbNewNodes * m * sizeof(int));				testError(__LINE__);
			cudaMalloc(&possiblyDisappeared_buffer,
					   ((2 * n) % 8 == 0 ? (2 * n) / 8 : (2 * n) / 8 + 1) *
					   nbNewNodes);				testError(__LINE__);
			
			cudaMemcpy(device_bitmap, bitmap, allocated_size,
					   cudaMemcpyHostToDevice);									testError(__LINE__);
			
			cudaMemcpy(device_vars, selectedVars, nbSelected*sizeof(int),
					   cudaMemcpyHostToDevice);									testError(__LINE__);
			
			//Function call
			dim3 dimBlock(NB_THREADS_PER_BLOCK);
			dim3 dimGrid(nbNewNodes % dimBlock.x == 0 ?
						 nbNewNodes / dimBlock.x : nbNewNodes / dimBlock.x + 1);

			exploreOneParallel<<<dimGrid, dimBlock>>>
						(device_output, device_bitmap, device_vars, n, m,
						 nbSelected, allocated_size, queues_size,
						 toAffect_buffer, temp_buffer, toPropagate_buffer,
						 recentlySolved_buffer, possiblyDisappeared_buffer);				testError(__LINE__);
			
			cudaThreadSynchronize();											testError(__LINE__);
			
			
			//Getting back the results
			for(int i=0; i<nbNewNodes; i++)
			{
				Node node(n,m);
				
				cudaMemcpy(node.bitmap, device_output+i*allocated_size, allocated_size,
						   cudaMemcpyDeviceToHost);								testError(__LINE__);
				
				if(node.isSolvable())
				{
					result.push_back(node);
				}
			}

			//Free allocated memory
			cudaFree(device_bitmap);							testError(__LINE__);
			cudaFree(device_vars);					testError(__LINE__);
			cudaFree(device_output);				testError(__LINE__);
			cudaFree(toAffect_buffer);				testError(__LINE__);
			cudaFree(temp_buffer);				testError(__LINE__);
			cudaFree(toPropagate_buffer);				testError(__LINE__);
			cudaFree(recentlySolved_buffer);				testError(__LINE__);
			cudaFree(possiblyDisappeared_buffer);				testError(__LINE__);
		}
	}
	
	return(result);
}



